$\forall$$A$:MsgA, $x$:Id, $k$:Knd.
\\[0ex]($\neg$$A$.frame($k$ affects $x$)) $\Rightarrow$ Feasible($A$) $\Rightarrow$ ($\neg$($\uparrow<$$k$, $x$$>$ $\in$ dom(($A$.2.2.2.2).1)))